////////////////// ERROR-HANDLING  //////////////////////////////////////////////////////

  function UserError(code, parameters, messages) {
    this.code = code;
    this.parameters = parameters || {};
    this.messages = messages || [];
  }
  // TODO: fix this
  //UserError.prototype = new Error();
  //UserError.prototype.constructor = UserError();

 /** 
  * @param error: a UserError object
  * @param errorDictionary: a dictionary keyed by error codes for each of which
  *        it provides a description of possible ways to display the error to 
  *        the user, one of which will be chosen at random.
  * @param language: the relevant Language
  * @result A string to show to the user describing what went wrong.
  */
  var renderError = function(error, errorDictionary, language) {
    if (error.code === 'pre-rendered') {
      return error.messages[Math.floor((Math.random()*error.messages.length))];
    } else {
      if (!errorDictionary.hasOwnProperty(error.code)) {
        throw new Error('Unknow error code ' + error.code + ' sent to renderError().');
      }
      var messageTemplates = errorDictionary[error.code].templates;
      var messageTemplate = messageTemplates[Math.floor((Math.random()*messageTemplates.length))];
      var message = '';
      for (var i = 0; i < messageTemplate.length; i++) {
        if (messageTemplate[i].isFixed) {
          message += messageTemplate[i].content;
        } else {
          var parameterFormat = errorDictionary[error.code].parameters[messageTemplate[i].content].format;
          var parameter = error.parameters[messageTemplate[i].content];
          switch (parameterFormat) {
            case 'string':
              message += parameter;
              break;
            case 'expression':
              message += displayExpression(parameter, language.operators);
              break;
            default:
              throw Error('Uknown format ' + parameterFormat + ' sent to renderError().');
          }
        }
      }
      return message;
    }
  }

///////////////////  DISPLAY  ////////////////////////////////////////////////////////////

 /** 
  * @param expression: an Expression, which is to be displayed
  * @param operators: provides the symbols keys of the operators so that we
  *        we know e.g. 'for_all' should be displayed using '@'.
  * @param used internally to determine whether to surround the formula with 
  *        brackets; when calling this function it should not be provided.
  * @result A string representing the expression that can be shown to the user.
  */
  // FUTURE: replace this with a generalised system that reads from 
  // kinds.display using a rewritten displayExpressionFragment
  var displayExpression = function(expression, operators, levelAboveNumActive) {
    levelAboveNumActive = levelAboveNumActive || 0;
    // thisLevelNumActive provides the levelAboveNumActive for the level below
    if (expression.kind === 'binary_connective' || expression.kind === 'binary_relation' || expression.kind === 'binary_function') {
      var thisLevelNumActive = 2;
    } else if (expression.kind === 'unary_connective' || expression.kind === 'quantifier') {
      var thisLevelNumActive = 1;
      // NOTE: it would be preferable if bounded_quantifier had thisLevelNumActive for its second argument only
    } else {
      var thisLevelNumActive = 0;
    }
    var processedArguments = [];
    var processedDummies = [];
    for (var i = 0; i < expression.arguments.length; i++) {
      processedArguments.push(displayExpression(expression.arguments[i], operators, thisLevelNumActive));
    }
    for (var i = 0; i < expression.dummies.length; i++) {
      processedDummies.push(displayExpression(expression.dummies[i], operators, thisLevelNumActive));
    }

    var symbol = (!operators.hasOwnProperty(expression.operator)) ? expression.operator:
      (!operators[expression.operator].hasOwnProperty('symbols')) ? expression.operator:
      operators[expression.operator].symbols[0];

    if (expression.kind === 'binary_connective' || expression.kind === 'binary_relation' || expression.kind === 'binary_function') {
      return (levelAboveNumActive > 0) ? "(" + processedArguments.join(symbol) + ")":
        processedArguments.join(symbol);
    } else if (expression.kind === 'unary_connective') {
      return symbol + processedArguments[0];
    } else if (expression.kind === 'quantifier') {
      var output = symbol + processedDummies[0] + '.' + processedArguments[0]; 
      return (levelAboveNumActive === 2) ? "(" + output + ")": output;
    } else if (expression.kind === 'bounded_quantifier') {
      var output = symbol + processedArguments[0] + '.' + processedArguments[1];
      return (levelAboveNumActive === 2) ? "(" + output + ")": output;
    } else if (expression.kind === 'prefix_relation' || expression.kind === 'prefix_function') {
      return symbol + "(" + processedArguments.join(",") + ")";
    } else if (expression.kind === 'ranged_function') {
      return symbol + '{' + processedArguments[0] + ' | ' + processedArguments[1] + '}';
    } else if (expression.kind === 'atom' || expression.kind === 'constant' || expression.kind === 'variable') {
      return symbol;
    } else {
      throw Error('Unknown kind ' + expression.kind + ' sent to displayExpression()');
    }
  };

  var displayExpressionArray = function(expressionArray, operators) {
    var processedArray = [];
    for (var i = 0; i < expressionArray.length; i++) {
      processedArray.push(displayExpression(expressionArray[i], operators));
    }
    return processedArray.join(", ");
  }

  // Only used for testing so far
  var displayExpressionDictionary = function(expressionDictionary, operators) {
    var processedArray = [];
    for (var key in expressionDictionary) {
      processedArray.push(key + ':' + displayExpression(expressionDictionary[key], operators));
    }
    return processedArray.join(", ");
  }




///////////////////////////  PARSING  ///////////////////////////////////////////////////////////////////////////

 /** 
  * This function checks whether the string contains any symbol that occurs 
  * in a member of the symbols key for an operator (these will be
  * symbols such as @, =, <).
  */
  var containsLegalSymbol = function(string, operators, isTemplate) {
    for (var i = 0; i < ['(', ')', ','].length; i++) {
      if (string.indexOf(['(', ')', ','][i]) !== -1) {
        return true;
      }
    }
    for (var i = 0; i < ['[', '-', '>', '|', ']', '}', '{'].length; i++) {
      if (isTemplate && string.indexOf(['[', '-', '>', '|', ']', '}', '{'][i]) !== -1) {
        return true;
      }
    }
    for (var key in operators) {
      if (operators[key].hasOwnProperty('symbols')) {
        for (var i = 0; i < operators[key].symbols.length; i++) {
          // we dismember multi-character symbols.
          for (var j = 0; j < operators[key].symbols[i].length; j++) {
            if (string.indexOf(operators[key].symbols[i][j]) !== -1) {
              return true;
            }
          }
        }
      }
    }
    return false;
  };

 /** 
  * This function strips whitespace from within expressions, whilst using the
  * whitespace between expressions to split a line into an array of word / 
  * expression strings. It also identifies any illegal symbols.
  * e.g. 'from p and q we have p & q' will be converted to ['from', 'p',
  *   'and', 'q', 'we', 'have', 'p&q'].
  */
  var preParseLine = function(input, operators, isTemplate) {
    isTemplate = isTemplate || false;

    var n = 0;
    while(input[n] === ' ') {
      n++;
    }
    if (n%2 === 0 || isTemplate) {
      var indentation = n/2;
    } else {
      throw new UserError('odd_number_spaces', {});
    }

    var output = [];
    var currentWord = '';
    var justPassedSymbol = false;
    var justPassedSpace = false;
    for (var i = n; i < input.length; i++) {
      if (/^[A-Za-z0-9()]/.test(input[i]) || (isTemplate && [']', '{', '}'].indexOf(input[i]) !== -length-1)) {
        if (justPassedSpace && input[i] !== ')' && input[i] !== '}' && input[i] !== ']') {
          output.push(currentWord);
          currentWord = input[i];
        } else {
          currentWord += input[i];
        }
        justPassedSpace = false;
        justPassedSymbol = (input[i] === '(' || input[i] === '{');
      } else if (input[i] === ' ') {
        if (!justPassedSymbol) {
          justPassedSpace = true;
        }
      } else if (containsLegalSymbol(input[i], operators, isTemplate)) {
        if (justPassedSpace && (input[i] === '@' || input[i] === '$' || input[i] === '~')) {
          output.push(currentWord);
          currentWord = input[i];
        } else {
          currentWord += input[i];
        }
        justPassedSpace = false;
        justPassedSymbol = true;
      } else {
        throw new UserError('illegal_symbol', {symbol: input[i]});
      }
    }
    if (currentWord !== '') {
      output.push(currentWord);
    }
    if (output.length === 0) {
      throw new UserError('blank_line', {})
    }
    if (isTemplate) {
      return {output: output};
    } else {
      return {
        output: output,
        indentation: indentation
      }
    }
  };

 /**
  * @param inputString: written by the user - we will parse it.
  * @param operators: the relevant operators, which are just needed for their
  *        symbols so we can identify whether the symbols the user is using are
  *        legitimate.
  * @param vocabulary: we will attempt to match sections of the inputString to
  *        vocabulary entries.
  * @param isTemplate: if true, we parse the input as a LineTemplate; otherwise
  *        we parse it as a Line.
  * @result A LineTemplate.reader_view if isTemplate === true, and a ProtoLine if
  *         isTemplate === false.
  */
  var parseLine = function(inputString, operators, vocabulary, isTemplate) {
    var preParse = preParseLine(inputString, operators, isTemplate);

    // We compile all words occurring in the vocabulary, to help us identify
    // them in lines.
    var vocabularyWords = [];
    for (var key in vocabulary) {
      for (var i = 0; i < vocabulary[key].length; i++) {
        for (var j = 0; j < vocabulary[key][i].split(' ').length; j++) {
          if (vocabularyWords.indexOf(vocabulary[key][i].split(' ')[j]) === -1) {
            vocabularyWords.push(vocabulary[key][i].split(' ')[j]);
          } 
        }
      }
    }

    var unmatchedArray = preParse.output;
    // The lth entry in this array will contain all matchings of the first 
    // l-many elements of the unmatchedArray.
    var partiallyMatchedArrays = [[[]]];
    for (var i = 1; i <= unmatchedArray.length; i++) {
      partiallyMatchedArrays.push([]);
    }

    for (var l = 0; l < unmatchedArray.length; l++) {
      // We have matched the first l-many entries in the given unmatchedArray,
      // and will now attempt to match the next one.

      // This will only occur in pathological cases
      if (partiallyMatchedArrays[l].length > 1000) {
        throw new UserError('too_many_parsings', {});
      }

      for (var k = l + 1; k <= unmatchedArray.length; k++) {
        for (var key in vocabulary) {
          for (var i = 0; i < vocabulary[key].length; i++) {
            if (unmatchedArray.slice(l, k).join(' ').toLowerCase() === vocabulary[key][i]) {
              // We have identified the next (k-l)-many words together form a
              // phrase in the vocabulary dictionary.
              for (var j = 0; j < partiallyMatchedArrays[l].length; j++) {
                partiallyMatchedArrays[k].push(partiallyMatchedArrays[l][j].concat([{
                  format: 'phrase',
                  content: key
                }]))
              }
            }
          }
        }
      }

      if (vocabularyWords.indexOf(unmatchedArray[l].toLowerCase()) === -1 || unmatchedArray[l].length === 1) {
        // We attempt to parse this entry as an expression / expression template
        try {
          var expression = (isTemplate) ? 
            parser.parse(unmatchedArray[l], 'expressionTemplate'):
            parser.parse(unmatchedArray[l], 'expression');
          for (var j = 0; j < partiallyMatchedArrays[l].length; j++) {
            // We do not allow a line to have two expressions in a row. This is to
            // allow the identification of typos: For example if the user types 
            // 'fron p&q ...' then otherwise we would think that both 'fron' and
            // 'p&q' are expressions. We also do not attempt to parse a word as an
            // expression if it is a vocabulary word, to avoid masses of silly 
            // attempts to parse the line.
            if (l === 0 || partiallyMatchedArrays[l][j][partiallyMatchedArrays[l][j].length - 1].format === 'phrase') {
              partiallyMatchedArrays[l+1].push(partiallyMatchedArrays[l][j].concat([{
                format: 'expression',
                content: expression
              }]))
            }
          }
        }
          catch(err) {}
      }
    }

    if (partiallyMatchedArrays[unmatchedArray.length].length > 0) {
      // We have succeeded in fully matching
      return (isTemplate) ?
        {results: partiallyMatchedArrays[unmatchedArray.length]}:
        {
          results: partiallyMatchedArrays[unmatchedArray.length],
          indentation: preParse.indentation
        };

    } else {
      // We identify the best attempt
      var numEntriesMatched = 0;
      for (var i = 0; i <= unmatchedArray.length; i++) {
        if (partiallyMatchedArrays[i].length > 0) {
          numEntriesMatched = i;
        }
      }
      // We return the best description of the problem we can
      var bestAttempt = partiallyMatchedArrays[numEntriesMatched][0];
      if (numEntriesMatched === 0 || bestAttempt[bestAttempt.length-1].format === 'phrase') {
        var word = unmatchedArray[numEntriesMatched];
        throw (vocabularyWords.indexOf(word) !== -1) ?
          new UserError('unidentified_phrase', {word: word}):
          new UserError('unidentified_word', {word: word})
      } else {
        var word1 = unmatchedArray[numEntriesMatched - 1];
        var word2 = unmatchedArray[numEntriesMatched];
        if (vocabularyWords.indexOf(word1) !== -1) {
          throw new UserError('unidentified_phrase', {word: word1});
        } else if (containsLegalSymbol(word1, operators, isTemplate)) {
          throw (vocabularyWords.indexOf(word2) !== -1) ?
            new UserError('unidentified_phrase', {word: word2}):
            (containsLegalSymbol(word2, operators, isTemplate)) ?
              new UserError('consecutive_expressions', {word1: word1, word2: word2}):
              new UserError('unidentified_word', {word: word2})
        } else {
          throw (vocabularyWords.indexOf(word2) !== -1) ?
            new UserError('unidentified_phrase', {word: word2}):
            (containsLegalSymbol(word2, operators, isTemplate)) ?
              new UserError('unidentified_word', {word: word1}):
              new UserError('unidentified_words', {word1: word1, word2: word2});
        }
      }
    }
  };

////////////////////  TYPING ASSIGNMENT /////////////////////////////////////////////////////////////////////////////////////////////////////

 /**
  * @param types: an array of types, potentially ending with null, as found in
  *        a TypingRule.
  * @param desiredLength: the number of entries we would like to have.
  * @result: an array of types with the right number of entries, derived from
  *          'types'.
  * An error is throw if such a thing is not possible.
  */
  var instantiateTypingRule = function(types, desiredLength) {
    if (types[types.length - 1] === null) {
      var output = [];
      if (types.length <= desiredLength + 2) {
        for (var i = 0; i < types.length - 2; i++) {
          output.push(types[i]);
        }
        for (var i = types.length-2; i<desiredLength; i++) {
          output.push(types[types.length-2]);
        }
        return output;
      } else {
        throw new UserError('not_enough_inputs', {num_needed: desiredLength});
      }
    } else {
      if (types.length === desiredLength) {
        return types;
      } else {
        throw new UserError('wrong_num_inputs', {num_needed: desiredLength});
      }
    }
  };

 /**
  * This takes an (untyped) Expression, usually provided by the parser, and
  * returns a TypedExpression in which types have been added at each level.
  * @param untypedExpression: the expression to be typed
  * @param possibleTopTypes: an array of types that the expression as a whole
  *        could have - each will be tried in turn.
  * @param language: the relevant language
  * @param newKindsPermitted: an array of kinds (e.g. 'variable', 'constant')
  *        of which the user is allowed to create new operators. Any operator
  *        with a kind not in this list and that does not already occur in the
  *        language will cause an error.
  * @param permitDuplicateDummyNames: if true the user can write e.g. @x.p even
  *        if x is already in use; if false they cannot.
  * @result An array of dictionaries of the form: {
  *           typedExpression: A TypedExpression
  *           operators: the given language.operatorss together with any new
  *             operators that occurred in the expression.
  *         }
  * If a valid typing cannot be found this function will throw a UserError. The
  * parameters of this error will contain an additional key 'amountTyped' that
  * determines where the error occurred. e.g. [1,2,0] would indicate that there
  * was a problem at the 0th input (dummy or argument) of the 2nd input of the 
  * 1st input of this expression. We return the typing attempt for which this 
  * value is largest (in lexicographic ordering) as this is likely to be
  * closest to what the user intended.
  */
  var assignTypesToExpression = function(untypedExpression, possibleTopTypes, language, newKindsPermitted, permitDuplicateDummyNames) {
    var operators = language.operators;
    newKindsPermitted = newKindsPermitted || ['constant', 'variable'];
    permitDuplicateDummyNames = permitDuplicateDummyNames || false;

    var _attemptTyping = function(topType, typingRule) {

      if (!operatorIsNew && untypedExpression.kind !== operators[untypedExpression.operator].kind) {
        throw new UserError('wrong_kind', {
          operator: untypedExpression.operator, 
          expected_kind: operators[untypedExpression.operator].kind,
          actual_kind: untypedExpression.kind,
          amount_typed: []
        });
      }
      if (topType !== typingRule.output) {
        throw new UserError('wrong_type', {
          operator: untypedExpression.operator,
          expected_type: topType,
          actual_type: typingRule.output,
          amount_typed: []
        });
      }

      var _isNumber = function(n){return !isNaN(parseFloat(n)) && isFinite(n);}
      var _isString = function(s){return s[0] === '\'' && s[s.length-1] === '\''}
      if (language.types.hasOwnProperty('integer') && 
          _isNumber(untypedExpression.operator) && untypedExpression.kind === 'constant' &&
          topType !== 'integer') {
        throw new UserError('wrong_type', {
          operator: untypedExpression.operator,
          expected_type: topType,
          actual_type: 'integer',
          amount_typed: []
        })
      }
      if (language.types.hasOwnProperty('string') && 
          _isString(untypedExpression.operator) && untypedExpression.kind === 'constant' &&
          topType !== 'string') {
        throw new UserError('wrong_type', {
          operator: untypedExpression.operator,
          expected_type: topType,
          actual_type: 'string',
          amount_typed: []
        })
      }

      try {
        var argumentTypes = instantiateTypingRule(typingRule.arguments, untypedExpression.arguments.length);
      }
      catch (err) {
        err.parameters['operator'] = untypedExpression.operator;
        err.parameters['input_category'] = 'arguments';
        err.parameters['amount_typed'] = [];
        throw err;
      }
      try {
        var dummyTypes = instantiateTypingRule(typingRule.dummies, untypedExpression.dummies.length);
      }
      catch (err) {
        err.parameters['operator'] = untypedExpression.operator;
        err.parameters['input_category'] = 'dummies';
        err.parameters['amount_typed'] = [];
        throw err;
      }
      var updatedOperators = {};
      for (key in operators) {
        updatedOperators[key] = operators[key];
      }
      if (operatorIsNew) {
        updatedOperators[untypedExpression.operator] = {
          kind: untypedExpression.kind,
          typing: [{
            arguments: argumentTypes,
            dummies: dummyTypes,
            output: topType
          }]
        };
      }

      for (var i = 0; i < untypedExpression.dummies.length; i++) {
        if (!permitDuplicateDummyNames && updatedOperators.hasOwnProperty(untypedExpression.dummies[i].operator)) {
          throw new UserError('duplicate_dummy_name', {
            dummy: untypedExpression.dummies[i],
            expression: untypedExpression,
            amount_typed: []
          });
        } else if (untypedExpression.dummies[i].kind !== 'variable'){
          // The parser does not currently permit this to happen
          throw new UserError('dummy_not_variable', {
            dummy: untypedExpression.dummies[i],
            expression: untypedExpression,
            amount_typed: []
          });
        }
      }

      return assignTypesToExpressionArray(
        untypedExpression.dummies.concat(untypedExpression.arguments), 
        dummyTypes.concat(argumentTypes), {
          operators: updatedOperators,
          kinds: language.kinds,
          types: language.types
        }, newKindsPermitted, permitDuplicateDummyNames, 
        untypedExpression.dummies.length);
    };

    var operatorIsNew = false;
    if (!operators.hasOwnProperty(untypedExpression.operator)) {
      if (newKindsPermitted.indexOf(untypedExpression.kind) === -1) {
        throw new UserError('unknown_operator', {operator: untypedExpression.operator, amount_typed: []});
      } else {
        operatorIsNew = true;
      }
    }
    var typingRules = (operatorIsNew) ?
      language.kinds[untypedExpression.kind].typing: 
      operators[untypedExpression.operator].typing;

    var results = [];
    for (var l = 0; l < possibleTopTypes.length; l++) {
      for (var k = 0; k < typingRules.length; k++) {

        try {
          var newAttempts = _attemptTyping(possibleTopTypes[l], typingRules[k]);
          for (var j = 0; j < newAttempts.length; j++) {
            var typedDummies = [];
            for (var i = 0; i < untypedExpression.dummies.length; i++) {
              typedDummies.push(newAttempts[j].typedArray[i]);
              // These dummy variables should not be available outside this
              // part of the untypedExpression.
              if (!operators.hasOwnProperty(untypedExpression.dummies[i].operator)) {
                delete newAttempts[j].operators[untypedExpression.dummies[i].operator];
              }
            }
            var typedArguments = [];
            for (var i = untypedExpression.dummies.length; i < untypedExpression.dummies.length + untypedExpression.arguments.length; i++) {
              typedArguments.push(newAttempts[j].typedArray[i]);
            }

            results.push({
              typedExpression: {
                operator: untypedExpression.operator,
                kind: untypedExpression.kind,
                arguments: typedArguments,
                dummies: typedDummies,
                type: possibleTopTypes[l]
              },
              operators: newAttempts[j].operators
            });
          }
        }
        catch (err) {
          if (bestAttemptSoFar === undefined || greaterThanInLex(err.parameters.amount_typed, bestAttemptSoFar.parameters.amount_typed)) {
            var bestAttemptSoFar = err;
          }
        }
      }
    }
    if (results.length > 0) {
      return results;
    } else {
      throw bestAttemptSoFar;
    }
  };

 /** Companion function to assignTypesToExpression, with the following
  * modifications:
  * @param untypedArray: an array of expressions to type
  * @param topTypes: an array of types that the expressions in the array must
  *        have (only one option for each).
  * @numDummies: the number of elements in the array (from the start) that are
  *              dummies rather than arguments.
  * @result: {
  *            typedArray: an array of TypedExpressions
  *            operators: the updated list of operators
  *          }
  */
  var assignTypesToExpressionArray = function(untypedArray, topTypes, language, newKindsPermitted, isTemplate, numDummies) {
    newKindsPermitted = newKindsPermitted || ['constant', 'variable'];
    isTemplate = isTemplate || false;
    numDummies = numDummies || 0;

    var partiallyTypedArrays = [[[]]];
    var partiallyUpdatedOperatorss = [[{}]];
    for (var key in language.operators) {
      partiallyUpdatedOperatorss[0][0][key] = language.operators[key];
    }
    for (var m = 1; m <= untypedArray.length; m++) {
      partiallyTypedArrays.push([]);
      partiallyUpdatedOperatorss.push([]);
    }

    for (var m = 0; m < untypedArray.length; m++) {

      // this will only happen in pathological cases
      if (partiallyTypedArrays[m].length > 1000) {
        throw new UserError('too_many_typings', {});
      }

      for (var n = 0; n < partiallyTypedArrays[m].length ; n++) {
        // Dummies are always allowed to have previously unseen names
        var newKindsPermittedHere = (m < numDummies) ? newKindsPermitted.concat(['variable']) : newKindsPermitted;
        try {
          var newResults = assignTypesToExpression(
            untypedArray[m], [topTypes[m]], {
              operators: partiallyUpdatedOperatorss[m][n],
              kinds: language.kinds,
              types: language.types
            }, newKindsPermittedHere, isTemplate);
          for (var i = 0; i < newResults.length; i++) {
            partiallyTypedArrays[m + 1].push(partiallyTypedArrays[m][n].concat([newResults[i].typedExpression]));
            partiallyUpdatedOperatorss[m + 1].push(newResults[i].operators);
          }
        }
        catch (err) {
          var amountTyped = [m].concat(err.parameters.amount_typed);
          if (bestAttemptSoFar === undefined || greaterThanInLex(amountTyped, bestAttemptSoFar.parameters.amount_typed)) {
            err.parameters.amount_typed = amountTyped;
            var bestAttemptSoFar = err;
          }
        }
      }
    }
    var fullyTypedArrays = partiallyTypedArrays[untypedArray.length];
    var fullyUpdatedOperatorss = partiallyUpdatedOperatorss[untypedArray.length];
    if (fullyTypedArrays.length > 0) {
      var result = [];
      for (var i = 0; i < fullyTypedArrays.length; i++) {
        result.push({
          typedArray: fullyTypedArrays[i],
          operators: fullyUpdatedOperatorss[i]
        })
      }
      return result;
    } else {
      throw bestAttemptSoFar
    }
  };



//////////////////////////  UTILITIES /////////////////////////////////////////////////////////////////////////////////////////////

  // Expressions with different dummy variables are considered different
  var checkExpressionsAreEqual = function(expression1, expression2) {
    if (expression1.kind !== expression2.kind ||
        expression1.operator !== expression2.operator || 
        expression1.arguments.length !== expression2.arguments.length || 
        expression1.dummies.length !== expression2.dummies.length) {
      return false;
    }
    if (expression1.hasOwnProperty('type')) {
      if (expression1.type !== expression2.type) {
        return false;
      }
    }
    for (var i = 0; i < expression1.arguments.length + expression1.dummies.length; i++) {
      if (!checkExpressionsAreEqual((expression1.arguments.concat(expression1.dummies))[i], 
          (expression2.arguments.concat(expression2.dummies))[i])) {
        return false;
      }
    }
    return true;
  };

  var checkExpressionIsInSet = function(expression, set) {
    for (var i = 0; i < set.length; i++) {
      if (checkExpressionsAreEqual(expression, set[i])) {
        return true;
      }
    }
    return false;
  }

  var checkSetsOfExpressionsAreEqual = function(set1, set2) {
    for (var i = 0; i < set1.length; i++) {
      if (!checkExpressionIsInSet(set1[i], set2)) {
        return false;
      }
    }
    for (var i = 0; i < set2.length; i++) {
      if (!checkExpressionIsInSet(set2[i], set1)) {
        return false;
      }
    }
    return true;
  }

  // Returns a list of all the names of operators in an expression. kinds is an
  // array specifying which kinds of operators to return; if it is not supplied
  // then all are returned
  var getOperatorsFromExpression = function(expression, kinds) {
    kinds = kinds || false;
    var output = getOperatorsFromExpressionArray(expression.arguments.concat(expression.dummies), kinds);
    return (output.indexOf(expression.operator) === -1 && (kinds === false || kinds.indexOf(expression.kind) !== -1)) ? 
    output.concat([expression.operator]) : output;
  };  

  var getOperatorsFromExpressionArray = function(array, kinds) {
    kinds = kinds || false
    var output = [];
    for (var i = 0; i < array.length; i++) {
      var newOutput = getOperatorsFromExpression(array[i], kinds);
      for (var j = 0; j < newOutput.length; j++) {
        if (output.indexOf(newOutput[j]) === -1) {
          output = output.concat([newOutput[j]]);

        }
      }
    }
    return output;
  };

  // The expression should be typed; returns the type of operator (or false if
  // not found. Does not check for inconsistent typing.
  // NOTE: treats dummy variables like free ones.
  var seekTypeInExpression = function(expression, operator) {
    return operator === expression.operator ? expression.type:
      seekTypeInExpressionArray(expression.arguments.concat(expression.dummies), operator);
  };

  var seekTypeInExpressionArray = function(array, operator) {
    for (var i = 0; i < array.length; i++) {
      var attempt = seekTypeInExpression(array[i], operator);
      if (attempt !== false) {
        return attempt;
      }
    }
    return false;
  };

  // Returns whether LHS is larger than RHS in lexicographic ordering
  var greaterThanInLex = function (LHS, RHS) {
    for (var i = 0; i < LHS.length; i++) {
      if (i >= RHS.length) {
        return true;
      } else if (LHS[i] > RHS[i]) {
        return true;
      } else if (LHS[i] < RHS[i]) {
        return false;
      }
    }
    return false;
  }


/////////////////  DATAESQUE  ////////////////////////////////////////

  BASE_CONTROL_MODEL = {
    evaluation_rules: {
      'and': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          for (var i = 0; i < arguments.length; i++) {
            if (!arguments[i]) {
              return false;
            }
          }
          return true;
        }
      },
      'or': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          for (var i = 0; i < arguments.length; i++) {
            if (arguments[i]) {
              return true;
            }
          }
          return false;
        }
      },
      'not': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return !arguments[0];
        }
      },
      'implies': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return !arguments[0] || arguments[1];
        }
      },
      'iff': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return (arguments[0] && arguments[1]) || (!arguments[0] && !arguments[1]);
        }
      },
      'equals': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          if (types[0] === 'formula') {
            return checkExpressionsAreEqual(arguments[0], arguments[1]);
          } else if (arguments[0].type === 'set_of_formulas') {
            return checkSetsOfExpressionsAreEqual(arguments[0], arguments[1]);
          } else {
            return (arguments[0] === arguments[1]);
          }
        }
      },
      'not_equals': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          if (types[0] === 'formula') {
            return !checkExpressionsAreEqual(arguments[0], arguments[1]);
          } else if (arguments[0].type === 'set_of_formulas') {
            return !checkSetsOfExpressionsAreEqual(arguments[0], arguments[1]);
          } else {
            return (arguments[0] !== arguments[1]);
          }
        }
      },
      'less_than': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return (arguments[0] < arguments[1]);
        }
      },
      'less_than_or_equals': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return (arguments[0] <= arguments[1]);
        }
      },
      'greater_than': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return (arguments[0] > arguments[1]);
        }
      },
      'greater_than_or_equals': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return (arguments[0] >= arguments[1]);
        }
      },
      'is_in': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return checkExpressionIsInSet(arguments[0], arguments[1]);
        }
      },
      'addition': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return arguments[0] + arguments[1];
        }
      },
      'subtraction': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return arguments[0] - arguments[1];
        }
      },
      'multiplication': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return arguments[0] * arguments[1];
        }
      },
      'division': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return arguments[0] / arguments[1];
        }
      },
      'exponentiation': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return arguments[0] ^ arguments[1];
        }
      },
      'bounded_for_all': {
        format: 'top_down',
        content: function (expression, inputs, model, parameters, cache) {
          var newInputs = {};
          for (var key in inputs) {
            newInputs[key] = inputs[key];
          }
          var bounder = evaluate(expression.arguments[0].arguments[1], inputs, model, parameters, cache);
          if (expression.arguments[0].arguments[0].type === 'integer') {
            var rangeEnd = (expression.arguments[0].operator === 'less_than') ?
               bounder :
               bounder + 1;
            for (var i = 1; i < rangeEnd; i++) {
              newInputs[expression.dummies[0].operator] = i;
              if (!evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return false;
              }
            }
            return true;
          } else {
            // here the bounder is a set_of_formulas (so an array)
            for (var i = 0; i < bounder.length; i++) {
              newInputs[expression.dummies[0].operator] = bounder[i];
              if (!evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return false;
              }
            }
            return true;
          }
        }
      },
      'bounded_exists': {
        format: 'top_down',
        content: function (expression, inputs, model, parameters, cache) {
          var newInputs = {};
          for (var key in inputs) {
            newInputs[key] = inputs[key];
          }
          var bounder = evaluate(expression.arguments[0].arguments[1], inputs, model, parameters, cache);
          if (expression.arguments[0].arguments[0].type === 'integer') {
            var rangeEnd = (expression.arguments[0].operator === 'less_than') ?
               bounder :
               bounder + 1;
            for (var i = 1; i<rangeEnd; i++) {
              newInputs[expression.dummies[0].operator] = i;
              if (evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return true;
              }
            }
            return false;
          } else {
            // here the bounder is a set_of_formulas (so an array)
            for (var i = 0; i < bounder.length; i++) {
              newInputs[expression.dummies[0].operator] = bounder[i];
              if (evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return true;
              }
            }
            return false;
          }
        }
      },
      // min{k<n|A(k)} will range over [1,..,n-1], returning 0 if no match is found
      // min{p in antecedents(n)|A(p)} will range over antecedents(n), returning
      // the constant true if no match is found.
      'min': {
        format: 'top_down',
        content: function (expression, inputs, model, parameters, cache) {
          var newInputs = {};
          for (var key in inputs) {
            newInputs[key] = inputs[key];
          }
          var bounder = evaluate(expression.arguments[0].arguments[1], inputs, model, parameters, cache);
          if (expression.arguments[0].arguments[0].type === 'integer') {
            var rangeEnd = (expression.arguments[0].operator === 'less_than') ?
               bounder :
               bounder + 1;
            for (var i = 1; i < rangeEnd; i++) {
              newInputs[expression.dummies[0].operator] = i;
              if (evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return i;
              }
            }
            return 0;
          } else {
            for (var i = 0; i < bounder.length; i++) {
              newInputs[expression.dummies[0].operator] = bounder[i];
              if (evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return bounder[i];
              }
            }
            return {
              kind: 'constant',
              operator: true,
              arguments: [],
              dummies: []
            };
          }
        }
      },
      'max': {
        format: 'top_down',
        content: function (expression, inputs, model, parameters, cache) {
          var newInputs = {};
          for (var key in inputs) {
            newInputs[key] = inputs[key];
          }
          var bounder = evaluate(expression.arguments[0].arguments[1], inputs, model, parameters, cache);
          if (expression.arguments[0].arguments[0].type === 'integer') {
            var rangeEnd = (expression.arguments[0].operator === 'less_than') ?
               bounder :
               bounder + 1;
            for (var i = rangeEnd - 1; i > 0; i--) {
              newInputs[expression.dummies[0].operator] = i;
              if (evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return i;
              }
            }
            return 0;
          } else {
            for (var i = bounder.length-1; i >= 0; i--) {
              newInputs[expression.dummies[0].operator] = bounder[i];
              if (evaluate(expression.arguments[1], newInputs, model, parameters, cache)) {
                return bounder[i];
              }
            }
            return {
              kind: 'constant',
              operator: true,
              arguments: [],
              dummies: []
            };
          }
        }
      },
      // We subtract one for these because for the user proof lines are indexed from 1
      'indentation': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return parameters.proof.lines[arguments[0]-1].indentation;
        }
      },
      'template': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return '\'' + parameters.proof.lines[arguments[0]-1].template + '\'';
        }
      },
      'antecedents': {
        // NOTE: assumes antecedents are given as formulas, not integers
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          var antecedents = parameters.proof.lines[arguments[0]-1].antecedents;
          var output = [];
          for (var i = 0; i < antecedents.length; i++) {
            output.push(antecedents[i].content);
          }
          return output;
        }
      },
      'results': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return parameters.proof.lines[arguments[0]-1].results;
        }
      },
      'variables': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return parameters.proof.lines[arguments[0]-1].variables;
        }
      },
      'text': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return '\'' + parameters.proof.lines[arguments[0]-1].text + '\'';
        }
      },
      'element': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          // The name of the element is provided as a string such as \'R\', so
          // we must strip the quotes.
          var element = arguments[0].substr(1, arguments[0].length-2);
          return parameters.proof.lines[arguments[1]-1].elements[element];
        }
      },
      'num_lines': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return parameters.proof.lines.length;
        }
      },
      'assumptions': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return parameters.assumptions;
        }
      },
      'target': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return parameters.target;
        }
      },
      'question_variables': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          var names = getOperatorsFromExpressionArray(parameters.assumptions.concat([parameters.target]), ['variable']);
          // this gives us the variables as strings, we convert them to expressions
          var output = [];
          for (var i = 0; i < names.length; i++) {
            output.push({
              kind: 'variable',
              operator: names[i],
              arguments: [],
              dummies: []
            })
          }
          return output;
        }
      },
      'entry': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return arguments[1][arguments[0]-1];
        }
      },
      'if': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          return arguments[0] ? arguments[1]: arguments[2];
        }
      },
      'substitute': {
        format: 'bottom_up',
        content: function(arguments, types, parameters) {
          var substitutions = {};
          substitutions[arguments[1].operator] = arguments[2];
          return substituteIntoExpression(arguments[0], substitutions);
        }
      }
    }
  }
